Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
2023
Conference article
Open Access
A runtime environment for contract automata
Basile D., Ter Beek M. H.
Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 550–567, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_31
Metrics:
Basile D., Ter Beek M. H.
Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 550–567, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_31
Metrics:
See at:
ISTI Repository 
| link.springer.com 
| CNR ExploRA
2023
Conference article
Open Access
Mutant equivalence as monotonicity in parametric timed games
Basile D., Ter Beek M. H., Göttmann H., Lochau M.
The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.Source: FormaliSE'23 - 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 55–65, Melbourne, Australia, 14-15/05/2023
DOI: 10.1109/formalise58978.2023.00014
Metrics:
Basile D., Ter Beek M. H., Göttmann H., Lochau M.
The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.Source: FormaliSE'23 - 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 55–65, Melbourne, Australia, 14-15/05/2023
DOI: 10.1109/formalise58978.2023.00014
Metrics:
See at:
ISTI Repository | ieeexplore.ieee.org | CNR ExploRA
2023
Conference article
Open Access
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect
Basile D., Mazzanti F., Ferrari A.
The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL
Metrics:
Basile D., Mazzanti F., Ferrari A.
The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
Research challenges in orchestration synthesis
Basile D., Ter Beek M. H.
Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.Source: ICE 2023 - 16th Interaction and Concurrency Experience, Lisbon, Portugal, 19/6/2023
DOI: 10.4204/eptcs.383.5
Metrics:
Basile D., Ter Beek M. H.
Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.Source: ICE 2023 - 16th Interaction and Concurrency Experience, Lisbon, Portugal, 19/6/2023
DOI: 10.4204/eptcs.383.5
Metrics:
See at:
cgi.cse.unsw.edu.au | ISTI Repository | CNR ExploRA
2023
Software
Unknown
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect - Complementary data
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2023
Software
Unknown
A toolchain for strategy synthesis with spatial properties - Complementary material
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
See at: CNR ExploRA
2023
Report
Open Access
A sound and complete refinement relation for non-reducible modal transition systems
Basile D.
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Whenever two MTS are not in modal refinement relationship, it could still be the case that the set of implementations of one MTS is included in the set of implementations of the other. The challenge of devising an alternative notion of modal refinement that is both sound and complete with respect to the set of implementations, without disregarding valuable implementations, remains open. In this paper, we address this challenge. We introduce a subset of MTS called Non-reducible Modal Transition Systems (NMTS), together with a novel refinement relation for NMTS. We show that NMTS refinement is sound and also complete with respect to its set of implementations. We illustrate through examples how the additional constraints imposed by NMTS are necessary for achieving completeness. Furthermore, we discuss a property holding for NMTS whose implementations are non-deterministic. We show that any implementation obtained through modal refinement but disregarded by NMTS refinement is violating this property.Source: ISTI Working papers, 2023
DOI: 10.48550/arxiv.2310.08412
Metrics:
Basile D.
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Whenever two MTS are not in modal refinement relationship, it could still be the case that the set of implementations of one MTS is included in the set of implementations of the other. The challenge of devising an alternative notion of modal refinement that is both sound and complete with respect to the set of implementations, without disregarding valuable implementations, remains open. In this paper, we address this challenge. We introduce a subset of MTS called Non-reducible Modal Transition Systems (NMTS), together with a novel refinement relation for NMTS. We show that NMTS refinement is sound and also complete with respect to its set of implementations. We illustrate through examples how the additional constraints imposed by NMTS are necessary for achieving completeness. Furthermore, we discuss a property holding for NMTS whose implementations are non-deterministic. We show that any implementation obtained through modal refinement but disregarded by NMTS refinement is violating this property.Source: ISTI Working papers, 2023
DOI: 10.48550/arxiv.2310.08412
Metrics:
See at:
ISTI Repository | CNR ExploRA
2023
Report
Open Access
Modelling, verifying and testing the contract automata runtime environment with Uppaal
Basile D.
The contract automata runtime environment CARE is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling and verification of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilizing exhaustive and statistical model checking techniques. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and address the issues that have been identified and fixed.Source: ISTI Working papers, 2023
Basile D.
The contract automata runtime environment CARE is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling and verification of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilizing exhaustive and statistical model checking techniques. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and address the issues that have been identified and fixed.Source: ISTI Working papers, 2023
See at:
ISTI Repository | CNR ExploRA
2023
Software
Unknown
Modelling, verifying and testing the contract automata runtime environment with Uppaal: complementary data
Basile D.
This repository contains the complementary material for the paper: "Modelling and Verifying the Contract Automata Runtime Environment", Basile D. The latest version of the included files can be accessed through the GitHub repository of the Contract Automata Runtime Environment, https://github.com/contractautomataproject/CARE/tree/master/src/spec/uppaal In addition to the other contents, this Zenodo repository contains all the logs of the experiments.
Basile D.
This repository contains the complementary material for the paper: "Modelling and Verifying the Contract Automata Runtime Environment", Basile D. The latest version of the included files can be accessed through the GitHub repository of the Contract Automata Runtime Environment, https://github.com/contractautomataproject/CARE/tree/master/src/spec/uppaal In addition to the other contents, this Zenodo repository contains all the logs of the experiments.
See at: CNR ExploRA | zenodo.org
2023
Contribution to conference
Open Access
Research challenges in orchestration synthesis
Basile D.
This is the presentation of the paper "Research Challenges in Orchestration Synthesis" by Davide Basile and Maurice H. ter Beek, presented at the 16th Interaction and Concurrency Experience satellite workshop of the 18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, Lisbon, Portugal, 19-23/06/2023
Basile D.
This is the presentation of the paper "Research Challenges in Orchestration Synthesis" by Davide Basile and Maurice H. ter Beek, presented at the 16th Interaction and Concurrency Experience satellite workshop of the 18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, Lisbon, Portugal, 19-23/06/2023
See at:
ISTI Repository | youtu.be | CNR ExploRA
2023
Contribution to conference
Open Access
Experimenting with formal verification and model-based development: the case of UMC and Sparx EA
Basile D.
This is the presentation of "Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect" by Davide Basile, Franco Mazzanti, Alessio Ferrari, Presented at the 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023. https://doi.org/10.1007/978-3-031-43681-9_1Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, Antwerp, Belgium, 20-22/09/2023
Basile D.
This is the presentation of "Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect" by Davide Basile, Franco Mazzanti, Alessio Ferrari, Presented at the 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023. https://doi.org/10.1007/978-3-031-43681-9_1Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, Antwerp, Belgium, 20-22/09/2023
See at:
ISTI Repository | www.youtube.com | CNR ExploRA
2023
Contribution to conference
Open Access
A runtime environment for contract automata
Basile D.
This is the presentation of the paper "A Runtime Environment for Contract Automata", published at the 25th International Symposium on Formal Methods. The paper is available at https://doi.org/10.1007/978-3-031-27481-7_31Source: FM 2023 - Formal Methods: 25th International Symposium, Luebeck, Germany, 6-10/03/2023
Basile D.
This is the presentation of the paper "A Runtime Environment for Contract Automata", published at the 25th International Symposium on Formal Methods. The paper is available at https://doi.org/10.1007/978-3-031-27481-7_31Source: FM 2023 - Formal Methods: 25th International Symposium, Luebeck, Germany, 6-10/03/2023
See at:
ISTI Repository | youtu.be | CNR ExploRA
2023
Journal article
Open Access
A toolchain for strategy synthesis with spatial properties
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
See at:
ISTI Repository | ISTI Repository | CNR ExploRA
2022
Report
Open Access
A runtime environment for contract automata
Basile D., Ter Beek M. H.
Realising contract-based applications from formal specifications with formal guarantees requires to show the adherence of a specification, the contract, to its implementation. Contract automata have been introduced for specifying contract-based applications and synthesising their orchestrations as finite state automata. This paper introduces CARE, a newly developed library for implementing applications specified via contract automata, providing a runtime environment to coordinate services implementing contracts.Source: ISTI Working papers, pp.1–8, 2022
Basile D., Ter Beek M. H.
Realising contract-based applications from formal specifications with formal guarantees requires to show the adherence of a specification, the contract, to its implementation. Contract automata have been introduced for specifying contract-based applications and synthesising their orchestrations as finite state automata. This paper introduces CARE, a newly developed library for implementing applications specified via contract automata, providing a runtime environment to coordinate services implementing contracts.Source: ISTI Working papers, pp.1–8, 2022
See at:
arxiv.org | ISTI Repository | CNR ExploRA
2022
Software
Unknown
Contract automata runtime environment (v.1.0.0 - February 2022)
Basile D.
This document links the zenodo repository of CARE. Contract Automata Runtime Environment (v. February 2022) CARE is a library for implementing applications specified via contract automata. CARE provides a runtime environment to coordinate the CARE services that are implementing the contracts of the synthesised orchestration. Thus, CARE is the missing piece between specifications through contract automata and their implementations, so making explicit the low-level interactions realising the prescribed actions.DOI: 10.5281/zenodo.6393314
Metrics:
Basile D.
This document links the zenodo repository of CARE. Contract Automata Runtime Environment (v. February 2022) CARE is a library for implementing applications specified via contract automata. CARE provides a runtime environment to coordinate the CARE services that are implementing the contracts of the synthesised orchestration. Thus, CARE is the missing piece between specifications through contract automata and their implementations, so making explicit the low-level interactions realising the prescribed actions.DOI: 10.5281/zenodo.6393314
Metrics:
See at: CNR ExploRA
2022
Journal article
Open Access
Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods
Basile D., Ter Beek M. H., Ferrari A., Legay A.
Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using UPPAAL and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industrySource: International journal on software tools for technology transfer (Internet) 24 (2022): 351–370. doi:10.1007/s10009-022-00653-3
DOI: 10.1007/s10009-022-00653-3
Project(s): 4SECURAIL, ASTRail
Metrics:
Basile D., Ter Beek M. H., Ferrari A., Legay A.
Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using UPPAAL and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industrySource: International journal on software tools for technology transfer (Internet) 24 (2022): 351–370. doi:10.1007/s10009-022-00653-3
DOI: 10.1007/s10009-022-00653-3
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
link.springer.com | ISTI Repository | CNR ExploRA
2022
Journal article
Open Access
Contract automata library
Basile D., Ter Beek M. H.
Contract automata facilitate the specification, composition, and synthesis of behavioural contracts, comprehending modalities and configurations. Contract automata are supported by a software API called Contract Automata Library. This paper accompanies the software artefact by discussing its architecture, showing some usage examples and presenting recent improvements of the software in terms of quality, availability, usability, and documentation.Source: Science of computer programming (Print) 221 (2022). doi:10.1016/j.scico.2022.102841
DOI: 10.1016/j.scico.2022.102841
Metrics:
Basile D., Ter Beek M. H.
Contract automata facilitate the specification, composition, and synthesis of behavioural contracts, comprehending modalities and configurations. Contract automata are supported by a software API called Contract Automata Library. This paper accompanies the software artefact by discussing its architecture, showing some usage examples and presenting recent improvements of the software in terms of quality, availability, usability, and documentation.Source: Science of computer programming (Print) 221 (2022). doi:10.1016/j.scico.2022.102841
DOI: 10.1016/j.scico.2022.102841
Metrics:
See at:
ISTI Repository | Science of Computer Programming | www.sciencedirect.com | CNR ExploRA
2022
Journal article
Open Access
Static detection of equivalent mutants in real-time model-based mutation testing
Basile D., Ter Beek M., Lazreg S., Cordy M., Legay A.
Model-based mutation testing has the potential to effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue since it could produce many mutants that are equivalent to the original system model, making it impossible to generate test cases from them. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our empirical evaluation, based on a proof-of-concept implementation and a set of benchmarks from the literature, confirms the validity of our theory and demonstrates that in general our approach can avoid the generation of a significant amount of the equivalent mutants.Source: Empirical software engineering (Online) 7 (2022): 160–215. doi:10.1007/s10664-022-10149-y
DOI: 10.1007/s10664-022-10149-y
Metrics:
Basile D., Ter Beek M., Lazreg S., Cordy M., Legay A.
Model-based mutation testing has the potential to effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue since it could produce many mutants that are equivalent to the original system model, making it impossible to generate test cases from them. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our empirical evaluation, based on a proof-of-concept implementation and a set of benchmarks from the literature, confirms the validity of our theory and demonstrates that in general our approach can avoid the generation of a significant amount of the equivalent mutants.Source: Empirical software engineering (Online) 7 (2022): 160–215. doi:10.1007/s10664-022-10149-y
DOI: 10.1007/s10664-022-10149-y
Metrics:
See at:
link.springer.com | ISTI Repository | CNR ExploRA
2022
Journal article
Open Access
Empirical software engineering and formal methods for IoT systems
Basile D., Ter Beek M. H., Broccia G., Ferrari A.
Researchers from the Formal Methods and Tools (FMT) lab of ISTI-CNR are working on the application of formal methods to devise interaction protocols for safe-by-construction IoT Systems of Systems. They are also working on the empirical investigation and evaluation of the effectiveness of techniques and methodologies proposed for IoT application scenarios. The research is being conducted in the context of the national project T-LADIES, funded by the Italian Ministry of Education, University and Research (MIUR) under the program for Projects of National Interest (PRIN).Source: ERCIM news 131 (2022): 34–35.
Basile D., Ter Beek M. H., Broccia G., Ferrari A.
Researchers from the Formal Methods and Tools (FMT) lab of ISTI-CNR are working on the application of formal methods to devise interaction protocols for safe-by-construction IoT Systems of Systems. They are also working on the empirical investigation and evaluation of the effectiveness of techniques and methodologies proposed for IoT application scenarios. The research is being conducted in the context of the national project T-LADIES, funded by the Italian Ministry of Education, University and Research (MIUR) under the program for Projects of National Interest (PRIN).Source: ERCIM news 131 (2022): 34–35.
See at:
ercim-news.ercim.eu | ISTI Repository | CNR ExploRA
2022
Conference article
Open Access
An experimental toolchain for strategy synthesis with spatial properties
Basile D., Ter Beek M. H., Ciancia V.
We investigate the application of strategy synthesis to enforce spatial properties. The Contract Automata Library (CATLib) performs both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (VoxLogicA) is a spatial model checker that allows the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. In this paper, we explore the integration of these two tools. We provide a basic example of strategy synthesis on automata encoding motion of agents in spaces represented by images. The strategy is synthesised with CATLib, whilst the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 142–164, Rhodes, Greece, 24-28/10/2022
DOI: 10.1007/978-3-031-19759-8_10
Metrics:
Basile D., Ter Beek M. H., Ciancia V.
We investigate the application of strategy synthesis to enforce spatial properties. The Contract Automata Library (CATLib) performs both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (VoxLogicA) is a spatial model checker that allows the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. In this paper, we explore the integration of these two tools. We provide a basic example of strategy synthesis on automata encoding motion of agents in spaces represented by images. The strategy is synthesised with CATLib, whilst the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 142–164, Rhodes, Greece, 24-28/10/2022
DOI: 10.1007/978-3-031-19759-8_10
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA